Search Results

Documents authored by Markey, Nicolas

Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.32
Semilinear Representations for Series-Parallel Atomic Congestion Games

Authors: Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
We consider atomic congestion games on series-parallel networks, and study the structure of the sets of Nash equilibria and social local optima on a given network when the number of players varies. We establish that these sets are definable in Presburger arithmetic and that they admit semilinear representations whose all period vectors have a common direction. As an application, we prove that the prices of anarchy and stability converge to 1 as the number of players goes to infinity, and show how to exploit these semilinear representations to compute these ratios precisely for a given network and number of players.
Cite as

Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Semilinear Representations for Series-Parallel Atomic Congestion Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2022.32,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan},
  title =	{{Semilinear Representations for Series-Parallel Atomic Congestion Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.32},
  URN =		{urn:nbn:de:0030-drops-174243},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.32},
  annote =	{Keywords: congestion games, Nash equilibria, Presburger arithmetic, semilinear sets, price of anarchy}
}
Document
DOI: 10.4230/LIPIcs.TIME.2022.7
Logical Forms of Chronicles

Authors: Thomas Guyet and Nicolas Markey

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
A chronicle is a temporal model introduced by Dousson et al. for situation recognition. In short, a chronicle consists of a set of events and a set of real-valued temporal constraints on the delays between pairs of events. This work investigates the relationship between chronicles and classical temporal-model formalisms, namely TPTL and MTL. More specifically, we answer the following question: is it possible to find an equivalent formula in such formalisms for any chronicle? This question arises from the observation that a single chronicle captures complex temporal behaviours, without imposing a particular order of the events in time. For our purpose, we introduce the subclass of linear chronicles, which set the order of occurrence of the events to be recognized in a temporal sequence. Our first result is that any chronicle can be expressed as a disjunction of linear chronicles. Our second result is that any linear chronicle has an equivalent TPTL formula. Using existing expressiveness results between TPTL and MTL, we show that some chronicles have no equivalent in MTL. This confirms that the model of chronicle has interesting properties for situation recognition.
Cite as

Thomas Guyet and Nicolas Markey. Logical Forms of Chronicles. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{guyet_et_al:LIPIcs.TIME.2022.7,
  author =	{Guyet, Thomas and Markey, Nicolas},
  title =	{{Logical Forms of Chronicles}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.7},
  URN =		{urn:nbn:de:0030-drops-172542},
  doi =		{10.4230/LIPIcs.TIME.2022.7},
  annote =	{Keywords: temporal logics, temporal models}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.113
Parameterized Safety Verification of Round-Based Shared-Memory Systems

Authors: Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [James Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.
Cite as

Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized Safety Verification of Round-Based Shared-Memory Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 113:1-113:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.ICALP.2022.113,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sankur, Ocan and Waldburger, Nicolas},
  title =	{{Parameterized Safety Verification of Round-Based Shared-Memory Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{113:1--113:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.113},
  URN =		{urn:nbn:de:0030-drops-164541},
  doi =		{10.4230/LIPIcs.ICALP.2022.113},
  annote =	{Keywords: Verification, Parameterized models, Distributed algorithms}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.40
Dynamic Network Congestion Games

Authors: Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCGs, referred to as dynamic NCGs: in this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition. We study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure) Nash equilibria always exist in dynamic NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential time.
Cite as

Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Dynamic Network Congestion Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2020.40,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan},
  title =	{{Dynamic Network Congestion Games}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{40:1--40:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.40},
  URN =		{urn:nbn:de:0030-drops-132811},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.40},
  annote =	{Keywords: Congestion games, Nash equilibria, Subgame perfect equilibria, Complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.34
Dependences in Strategy Logic

Authors: Patrick Gardy, Patricia Bouyer, and Nicolas Markey

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: First, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2-EXPTIME under this new semantics.
Cite as

Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gardy_et_al:LIPIcs.STACS.2018.34,
  author =	{Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
  title =	{{Dependences in Strategy Logic}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.34},
  URN =		{urn:nbn:de:0030-drops-85320},
  doi =		{10.4230/LIPIcs.STACS.2018.34},
  annote =	{Keywords: strategic reasoning, strategy logic, dependences, behavioural strategies.}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2017.84
Temporal Logics for Multi-Agent Systems (Invited Talk)

Authors: Nicolas Markey

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
This is an overview of an invited talk delivered during the 42nd International Conference on Mathematical Foundations of Computer Science (MFCS 2017).
Cite as

Nicolas Markey. Temporal Logics for Multi-Agent Systems (Invited Talk). In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 84:1-84:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{markey:LIPIcs.MFCS.2017.84,
  author =	{Markey, Nicolas},
  title =	{{Temporal Logics for Multi-Agent Systems}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{84:1--84:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.84},
  URN =		{urn:nbn:de:0030-drops-81368},
  doi =		{10.4230/LIPIcs.MFCS.2017.84},
  annote =	{Keywords: Temporal logics, verification, game theory, strategic reasoning.}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.28
On the Expressiveness of QCTL

Authors: Amélie David, Francois Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
Cite as

Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{david_et_al:LIPIcs.CONCUR.2016.28,
  author =	{David, Am\'{e}lie and Laroussinie, Francois and Markey, Nicolas},
  title =	{{On the Expressiveness of QCTL}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.28},
  URN =		{urn:nbn:de:0030-drops-61643},
  doi =		{10.4230/LIPIcs.CONCUR.2016.28},
  annote =	{Keywords: Specification, Verification, Temporal Logic, Expressiveness, Tree automata}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.106
Reachability in Networks of Register Protocols under Stochastic Schedulers

Authors: Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
Cite as

Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 106:1-106:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2016.106,
  author =	{Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Sangnier, Arnaud and Stan, Daniel},
  title =	{{Reachability in Networks of Register Protocols under Stochastic Schedulers}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{106:1--106:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.106},
  URN =		{urn:nbn:de:0030-drops-62416},
  doi =		{10.4230/LIPIcs.ICALP.2016.106},
  annote =	{Keywords: Networks of Processes, Parametrized Systems, Stochastic Scheduler, Almost-sure Reachability, Cut-Off Property}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.69
Weighted Strategy Logic with Boolean Goals Over One-Counter Games

Authors: Patricia Bouyer, Patrick Gardy, and Nicolas Markey

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in [Mogavero et al. Reasoning about strategies: On the model-checking problem. ACM ToCL 15(4),2014]. As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.
Cite as

Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted Strategy Logic with Boolean Goals Over One-Counter Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 69-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2015.69,
  author =	{Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
  title =	{{Weighted Strategy Logic with Boolean Goals Over One-Counter Games}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{69--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.69},
  URN =		{urn:nbn:de:0030-drops-56537},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.69},
  annote =	{Keywords: Temporal logics, multi-player games, strategy logic, quantitative games}
}
Document
DOI: 10.4230/OASIcs.SynCoP.2015.48
Game-based Synthesis of Distributed Controllers for Sampled Switched Systems

Authors: Laurent Fribourg, Ulrich Kühne, and Nicolas Markey

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a centralized-controller synthesis technique based on state-space decomposition, and use a game-based approach to extend it to a distributed framework.
Cite as

Laurent Fribourg, Ulrich Kühne, and Nicolas Markey. Game-based Synthesis of Distributed Controllers for Sampled Switched Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 48-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fribourg_et_al:OASIcs.SynCoP.2015.48,
  author =	{Fribourg, Laurent and K\"{u}hne, Ulrich and Markey, Nicolas},
  title =	{{Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{48--62},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.48},
  URN =		{urn:nbn:de:0030-drops-56091},
  doi =		{10.4230/OASIcs.SynCoP.2015.48},
  annote =	{Keywords: Cyber-physical systems, controller synthesis, games, robustness, partial observation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.311
On the Value Problem in Weighted Timed Games

Authors: Patricia Bouyer, Samy Jaziri, and Nicolas Markey

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been identified for which optimal weight and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in weighted timed games. We then introduce a large subclass of weighted timed games (for which the undecidability proof above applies), and provide an algorithm to compute arbitrary approximations of the value in such games. To the best of our knowledge, this is the first approximation scheme for an undecidable class of weighted timed games.
Cite as

Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 311-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2015.311,
  author =	{Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
  title =	{{On the Value Problem in Weighted Timed Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{311--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.311},
  URN =		{urn:nbn:de:0030-drops-53863},
  doi =		{10.4230/LIPIcs.CONCUR.2015.311},
  annote =	{Keywords: Timed games, undecidability, approximation}
}
Document
DOI: 10.4230/DagRep.5.2.1
Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)

Authors: Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas

Published in: Dagstuhl Reports, Volume 5, Issue 2 (2015)

Abstract
In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and - as a special focus - connections with control engineering (supervisory control).
Cite as

Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas. Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). In Dagstuhl Reports, Volume 5, Issue 2, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{chatterjee_et_al:DagRep.5.2.1,
  author =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  title =	{{Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)}},
  pages =	{1--25},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{2},
  editor =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.2.1},
  URN =		{urn:nbn:de:0030-drops-50424},
  doi =		{10.4230/DagRep.5.2.1},
  annote =	{Keywords: non-zero-sum games, infinite games, multi-player games, partial-observation games, quantitative games, controller synthesis, supervisory control}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.121
Synchronizing Words for Weighted and Timed Automata

Authors: Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The problem of synchronizing automata is concerned with the existence of a word that sends all states of the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete. In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.
Cite as

Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi. Synchronizing Words for Weighted and Timed Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{doyen_et_al:LIPIcs.FSTTCS.2014.121,
  author =	{Doyen, Laurent and Juhl, Line and Larsen, Kim G. and Markey, Nicolas and Shirmohammadi, Mahsa},
  title =	{{Synchronizing Words for Weighted and Timed Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.121},
  URN =		{urn:nbn:de:0030-drops-48370},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.121},
  annote =	{Keywords: Synchronizing words, weighted automata, timed automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.351
Mixed Nash Equilibria in Concurrent Terminal-Reward Games

Authors: Patricia Bouyer, Nicolas Markey, and Daniel Stan

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.
Cite as

Patricia Bouyer, Nicolas Markey, and Daniel Stan. Mixed Nash Equilibria in Concurrent Terminal-Reward Games. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 351-363, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2014.351,
  author =	{Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
  title =	{{Mixed Nash Equilibria in Concurrent Terminal-Reward Games}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{351--363},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.351},
  URN =		{urn:nbn:de:0030-drops-48550},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.351},
  annote =	{Keywords: concurrent games, randomized strategy, Nash equilibria, undecidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.90
Shrinking Timed Automata

Authors: Ocan Sankur, Patricia Bouyer, and Nicolas Markey

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening these. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.
Cite as

Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking Timed Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 90-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{sankur_et_al:LIPIcs.FSTTCS.2011.90,
  author =	{Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas},
  title =	{{Shrinking Timed Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{90--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.90},
  URN =		{urn:nbn:de:0030-drops-33627},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.90},
  annote =	{Keywords: Timed automata, implementability, robustness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.375
Nash Equilibria in Concurrent Games with Büchi Objectives

Authors: Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We study the problem of computing pure-strategy Nash equilibria in multiplayer concurrent games with Büchi-definable objectives. First, when the objectives are Büchi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic Büchi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the Büchi automata are 1-weak.
Cite as

Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash Equilibria in Concurrent Games with Büchi Objectives. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 375-386, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2011.375,
  author =	{Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael},
  title =	{{Nash Equilibria in Concurrent Games with B\"{u}chi Objectives}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{375--386},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.375},
  URN =		{urn:nbn:de:0030-drops-33340},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.375},
  annote =	{Keywords: Concurrent games, Nash equilibria, B\"{u}chi Objectives}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.120
ATL with Strategy Contexts: Expressiveness and Model Checking

Authors: Arnaud Da Costa, François Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies. We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we~prove that their model-checking problems remain decidable by~designing a tree-automata-based algorithm for model-checking ATLsc* on the full class of $n$-player concurrent game structures.
Cite as

Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts: Expressiveness and Model Checking. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 120-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dacosta_et_al:LIPIcs.FSTTCS.2010.120,
  author =	{Da Costa, Arnaud and Laroussinie, Fran\c{c}ois and Markey, Nicolas},
  title =	{{ATL with Strategy Contexts: Expressiveness and Model Checking}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{120--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.120},
  URN =		{urn:nbn:de:0030-drops-28589},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.120},
  annote =	{Keywords: alternating temporal logic, agent, strategy quantifier}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.308
Computing Rational Radical Sums in Uniform TC^0

Authors: Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
A fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether $\sum_{i=1}^m C_i A_i^{X_i}$ is zero for given rational numbers $A_i$, $C_i$, $X_i$. It has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform TC0. This requires several significant departures from Blömer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in TC0.
Cite as

Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. Computing Rational Radical Sums in Uniform TC^0. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 308-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.FSTTCS.2010.308,
  author =	{Hunter, Paul and Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Computing Rational Radical Sums in Uniform TC^0}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{308--316},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.308},
  URN =		{urn:nbn:de:0030-drops-28739},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.308},
  annote =	{Keywords: Sum of square roots, Threshold circuits, Complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1339
On Termination for Faulty Channel Machines

Authors: Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.
Cite as

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination for Faulty Channel Machines. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.STACS.2008.1339,
  author =	{Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo\"{e}l and Schnoebelen, Philippe and Worrell, James},
  title =	{{On Termination for Faulty Channel Machines}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1339},
  URN =		{urn:nbn:de:0030-drops-13390},
  doi =		{10.4230/LIPIcs.STACS.2008.1339},
  annote =	{Keywords: Automated Verification, Computational Complexity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact